The present disclosure relates to solving a Constraint Satisfaction Problem (CSP) in general, and to solving a CSP that comprises constraints with cyclic dependencies, in particular.
In essence, a CSP is a set of constraints over variables. The CSP is satisfied if an assignment to all variables of the CSP holds all the constraints of the CSP. The CSP may define a wide range of problems, such as for example scheduling activities (e.g., scheduling classes to professors such that each professor's personal time limitations are honored and such that in each classroom there is only one class at a time), resource allocation (which resource should be allocated to which task, where there is a limited number of resources and each task may be fulfilled using different resources out of the available resources), route calculation (e.g., how to get from point A to point B, where there are a plurality of possible intermediate points between A and B), and the like.
A CSP may be defined by a triplet P=<V, D, C>, where V is a set of variables (e.g., V={v1, . . . , vn}), D is a set of finite domains (e.g., D={Dv1, . . . , Dvn}), and C is a set of constraints on the value of the variables (e.g., C={C1, . . . , Cm}). A variable from V is assigned a discrete value from D.
A constraint of a CSP may be expressed using a mathematical expression comprising variables, operators, constants and connectives. The expression may be formed over atomic constraints, also referred to as components, and composition operands such as ‘and’ (conjunction), ‘or’ (disjucntion’), → (implication), ⇄ (if and only if), or the like. For example (a>b) and (b>a) is a constraint comprising two components: a>b and b>a. As another example, (a>b) and ((x=1)→(a<b)) is a constraint comprising three components (a>b), (x=1), and (a<b). In some cases, there may be a plurality of constraints that are implicitly conjuncted into a single constraint.
A solution to the CSP is a single assignment of each variable of V, such that each value is selected from the pertinent domain of D, and all constraints are satisfied.
As stated above, CSPs are utilized in many different practical applications. One application is a use of a CSP in verification of a computerized device, such as a processor or a software module. A test generator, configured to generate a test to be executed/simulated during a verification phase, may generate the test based upon a satisfying assignment to one or more CSPs. A CSP may be utilized, for example, for solving scheduling activities in which computer jobs are scheduled. A CSP may be utilized, for example, for workforce management to determine a preferred allocation of personnel. A CSP may be utilized, for example, for route and place calculations.
There are a plurality of techniques to solve a CSP, such as for example Maintaining Arc Consistency (MAC), tree Search, constraint propagation, forward checking and the like.
A CSP solver may iteratively perform two actions: propagate implications of the constraints to remove values from the domains; and select a value to a variable based on the corresponding domain. In case a constraint is not satisfied or in case a domain is set to an empty set, backtracking may be performed to revoke a value selection. In some exemplary embodiments, the CSP solver may determine that the CSP cannot be assigned. For example, in case the propagation performed without any value selection induces that a domain is the empty set. As another example, the CSP may determine that based on past value selection, and as none of the past values is part of a satisfying assignment, the CSP is not satisfiable.
In some cases, there may be a cyclic dependency between two or more constraints of the CSP. In other words, in response to implications of a first constraint, implications may be performed in respect to a second constraint, and in response to the implications of the second constraint, implications may be further performed in respect to the first constraint.